(** LoopInvariant plugin*)